Nuprl Lemma : div_unique
13,42
postcript
pdf
a
:
,
n
:
,
p
,
q
:
. Div(
a
;
n
;
p
)
Div(
a
;
n
;
q
)
(
p
=
q
)
latex
Up
int
2
,
int
2
Definitions
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
P
&
Q
,
i
j
<
k
,
Div(
a
;
n
;
q
)
,
,
,
Lemmas
nat
plus
wf
,
nat
wf
,
div
nrel
wf
,
lt
transitivity
2
,
mul
cancel
in
lt
origin
a:
, n:
, p, q:. Div(a;n;p) 
Div(a;n;q) (p = q 
) a:, n:, p, q:. Div(a;n;p) Div(a;n;q) (p = q ) T Qx:A. B(x)
j < k